import java.util.HashMap;

import apron.Abstract1;
import apron.ApronException;
import apron.Environment;
import apron.Interval;
import apron.Linexpr1;
import apron.Manager;

/**
 * Wrapper of Apron::Abstract1, handles the cases when some of the variables are
 * set to bottom.
 * 
 */
public class MyAbstract {

	Abstract1 currState;
	HashMap<String, Boolean> bottomMap;

	@Override
	public String toString() {

		if (isBottom()) {
			return "<empty>";
		}
		return String.format("Abstract: %s ==== Bottom: %s",
				currState.toString(), bottomMap.toString());
	}

	@Override
	public boolean equals(Object obj) {
		if (!(obj instanceof MyAbstract)) {
			return false;
		}
		MyAbstract in = (MyAbstract) obj;
		boolean abstractResult = false;
		try {
			abstractResult = currState.isEqual(ManagerFactory.newManager(),
					in.currState);
		} catch (ApronException e) {
			e.printStackTrace();
		}
		boolean bottomResult = bottomMap.equals(in.bottomMap);
		return abstractResult && bottomResult;
	}

	@Override
	public int hashCode() {
		return getVaribaleValues().hashCode();
	}

	public String[] getVarNames() {
		return bottomMap.keySet().toArray(new String[0]);
	}

	public boolean isBottom() {
		for (String s : bottomMap.keySet()) {
			if (!bottomMap.get(s)) {
				return false;
			}
		}
		return true;
	}

	public MyAbstract(Abstract1 xa0, HashMap<String, Boolean> bottomMapIn) {
		currState = xa0;
		bottomMap = bottomMapIn;

	}

	public MyAbstract(HashMap<String, Interval> result, Manager managerIn) {
		HashMap<String, Boolean> newBottomMap = new HashMap<String, Boolean>();

		String[] bnames = result.keySet().toArray(new String[0]);
		Interval[] values = new Interval[bnames.length];
		for (int i = 0; i < bnames.length; i++) {
			if (result.get(bnames[i]).isBottom()) {
				values[i] = Utils.newTop();
				newBottomMap.put(bnames[i], true);
			} else {
				values[i] = result.get(bnames[i]);
				newBottomMap.put(bnames[i], false);
			}
		}

		Environment env = new Environment(bnames, new String[0]);

		try {
			Abstract1 newAbstract = new Abstract1(managerIn, env, bnames,
					values);

			bottomMap = newBottomMap;
			currState = newAbstract;

		} catch (ApronException e) {
			e.printStackTrace();
		}
	}

	public static MyAbstract copyCtor(MyAbstract a) {
		MyAbstract temp = MyAbstract.newBottom(a.getVarNames(),
				ManagerFactory.newManager());
		temp.copy(a);

		return temp;
	}

	public void copy(MyAbstract a) {
		HashMap<String, Interval> vals = a.getVaribaleValues();
		setAbstractWith(vals);
	}

	public static MyAbstract newBottom(String[] vars, Manager manager) {
		String[] bnames = vars;
		Environment env = new Environment(bnames, new String[0]);
		try {
			Abstract1 xa0 = new Abstract1(manager, env, bnames,
					Utils.createTopIntervals(bnames));

			HashMap<String, Boolean> bottomMap = new HashMap<String, Boolean>();
			for (String s : bnames) {
				bottomMap.put(s, true);

			}

			return new MyAbstract(xa0, bottomMap);
		} catch (Exception e) {
			System.out.print(e);
		}

		return null;
	}

	public static MyAbstract newTop(String[] vars, Manager manager) {
		String[] bnames = vars;
		Environment env = new Environment(bnames, new String[0]);
		try {
			Abstract1 xa0 = new Abstract1(manager, env, bnames,
					Utils.createTopIntervals(bnames));

			HashMap<String, Boolean> bottomMap = new HashMap<String, Boolean>();
			for (String s : bnames) {
				bottomMap.put(s, false);

			}

			return new MyAbstract(xa0, bottomMap);
		} catch (Exception e) {
			System.out.print(e);
		}

		return null;
	}

	public void initVarWithTop(String varName) {
		initVarWithValue(varName, Utils.newTop());
	}

	public void initVarWithValue(String varName, Interval value) {
		HashMap<String, Interval> values = getVaribaleValues();
		values.put(varName, value);
		setAbstractWith(values);
	}

	public void meet(MyAbstract a) {
		HashMap<String, Interval> varsAndValues = getVaribaleValues();
		HashMap<String, Interval> inputVarsAndValues = a.getVaribaleValues();

		HashMap<String, Interval> result = new HashMap<String, Interval>();

		for (String varName : getVarNames()) {
			result.put(varName, Utils.MeetIntervals(varsAndValues.get(varName),
					inputVarsAndValues.get(varName)));
		}

		setAbstractWith(result);

	}

	public void join(MyAbstract a) {
		HashMap<String, Interval> varsAndValues = getVaribaleValues();
		HashMap<String, Interval> inputVarsAndValues = a.getVaribaleValues();

		HashMap<String, Interval> result = new HashMap<String, Interval>();

		for (String varName : getVarNames()) {
			result.put(varName, Utils.JoinIntervals(varsAndValues.get(varName),
					inputVarsAndValues.get(varName)));
		}

		setAbstractWith(result);

	}

	private void setAbstractWith(HashMap<String, Interval> result) {
		MyAbstract newAbstract = new MyAbstract(result,
				ManagerFactory.newManager());
		this.currState = newAbstract.currState;
		this.bottomMap = newAbstract.bottomMap;

	}

	public void widen(MyAbstract a) {
		HashMap<String, Interval> varsAndValues = getVaribaleValues();
		HashMap<String, Interval> inputVarsAndValues = a.getVaribaleValues();

		HashMap<String, Interval> result = new HashMap<String, Interval>();

		for (String varName : getVarNames()) {
			result.put(varName,
					Utils.WidenIntervals(varsAndValues.get(varName),
							inputVarsAndValues.get(varName)));
		}

		setAbstractWith(result);

	}

	public void assign(Linexpr1 l, String assignee) {

		HashMap<String, Interval> varValues = getVaribaleValues();
		HashMap<String, Interval> expressionVarValues = Utils
				.getExpressionRelevantValues(varValues, l);

		MyAbstract afterCalc = calculateExpression(l, expressionVarValues,
				assignee);

		updateStateWith(afterCalc);

	}

	private MyAbstract calculateExpression(Linexpr1 l,
			HashMap<String, Interval> expressionVarValues, String assignee) {
		if (oneOfTheExpressionVarsIsBottom(expressionVarValues)) {
			expressionVarValues.put(assignee, Utils.newBottom());
			return new MyAbstract(expressionVarValues,
					ManagerFactory.newManager());
		}

		Environment e = l.getEnvironment();
		if (!e.hasVar(assignee)) {
			e = e.add(new String[] { assignee }, null);
			l.extendEnvironment(e);
		}
		String[] varNames = e.getIntVars();
		Interval[] varValues = Utils.getValuesOf(varNames, expressionVarValues);
		Manager b1 = ManagerFactory.newManager();
		Abstract1 xa0 = null, xa1 = null;
		try {
			xa0 = new Abstract1(b1, e, varNames, varValues);
			xa1 = xa0.assignCopy(b1, assignee, l, null);
		} catch (ApronException e1) {
			e1.printStackTrace();
		}

		HashMap<String, Boolean> newBottom = new HashMap<String, Boolean>();

		for (String var : varNames) {
			newBottom.put(var, false);
		}

		return new MyAbstract(xa1, newBottom);
	}

	private boolean oneOfTheExpressionVarsIsBottom(
			HashMap<String, Interval> expressionVarValues) {
		for (String s : expressionVarValues.keySet()) {
			if (expressionVarValues.get(s).isBottom()) {
				return true;
			}
		}
		return false;
	}

	private void updateStateWith(MyAbstract afterCalc) {
		HashMap<String, Interval> current = getVaribaleValues();
		HashMap<String, Interval> updated = afterCalc.getVaribaleValues();

		for (String var : current.keySet()) {
			if (updated.containsKey(var)) {
				current.put(var, updated.get(var));
			}
		}

		setAbstractWith(current);

	}

	private HashMap<String, Interval> getVaribaleValues() {
		return Utils.getVaribaleValues(currState, bottomMap,
				ManagerFactory.newManager());

	}
}
